/****************************************************************************
 * Elisa 1.0                                                                *
 *--------------------------------------------------------------------------*
 * Author: Laurent Granvilliers, Vincent Sorin                              *
 * Copyright (c) 2004 Laboratoire d'Informatique de Nantes Atlantique       *
 *--------------------------------------------------------------------------*
 * Elisa is distributed WITHOUT ANY WARRANTY. Read the associated           *
 * COPYRIGHT file for more details.                                         *
 *--------------------------------------------------------------------------*
 * elisa_constraint.h                                                       *
 ****************************************************************************/

/**
 * @file elisa_constraint.h
 * @brief Base classes for constraints.
 */

/**
 * @defgroup Constraint Constraint
 * @brief Classes for constraints.
 */


#ifndef _ELISA_CONSTRAINT_H
#define _ELISA_CONSTRAINT_H

#include <iostream>
#include <set>
#include <vector>
#include <boost/shared_ptr.hpp>

#include "elisa_defs.h"
#include "elisa_variable.h"
#include "elisa_expression.h"
#include "elisa_real_expr.h"


NAMESPACE_ELISA
/**
 * @ingroup Constraint
 * @class ConstraintRep
 * @brief Base class for constraint representation
 */
class ConstraintRep
{
public:
	/**
 	 * Print the constraint
 	 * @param os the stream where the constraint must be printed
 	 */
	virtual void print(std::ostream & os) const = 0;

	/**
 	 * Return the arity of the relation
 	 */
	int arity() const;

	/**
 	 * Destructor
 	 */
	virtual
	~ConstraintRep();

	/**
 	 * Computes in s the variables occurring in *this
 	 * @param s the set of var where the variable are put
 	 */
	virtual void toVariables(VarImplSet & s) const;

	/**
 	 * Returns the number of occurrences of v in *this
 	 */
	virtual int multiplicity(VariableImpl & v) const;

	/**
 	 * @brief init the Intenal Representation of the variables
 	 * @param st SearchTree
 	 */
	virtual void initVariableImplementation(SearchTree & searchTree, VarImplSet & s);

	/**
 	 * Insertion of a new expression in the last place
 	 * @param e the expression to add in the constraint
 	 */
	void addExpr(SymbolicExpression *e);

	/// @name Management of reference counter
	//@{
	/// Increases the counter
	int addRef();

	/// Decreases the counter
	int delRef();

	/// Returns the value of the counter
	int ref() const;

	//@}
protected:
	typedef boost::shared_ptr<SymbolicExpression> SymbolicExpressionPtr;

	// @var symbolic expressions that compose the constraint
	std::vector<SymbolicExpressionPtr> m_exprs;

	// @var Reference counter
	int m_nref;
};

/**
 * @ingroup Constraint
 * @class Constraint
 * @brief Base class for constraints (container for variables)
 */
class Constraint
{
public:
	/**
 	 * Constructor
 	 */
	Constraint(ConstraintRep *rep = 0)
		: m_rep(rep)
	{
	}

	/**
 	 * Destructor
 	 */
	virtual ~Constraint()
	{
	}

	/// @name Iterators over the set of variables
	//@{
	VarImplSet::iterator beginVar()
	{
		return m_vars.begin();
	}

	VarImplSet::const_iterator beginVar() const
	{
		return m_vars.begin();
	}

	VarImplSet::iterator endVar()
	{
		return m_vars.end();
	}

	VarImplSet::const_iterator endVar() const
	{
		return m_vars.end();
	}
	//@}

	/// @name Comparison: default comparison wrt. memory locations
	//@{
	virtual bool operator==(const Constraint & c) const
	{
		return (this == (&c));
	}

	virtual bool operator!=(const Constraint & c) const
	{
		return (this != (&c));
	}
	//@}

	/**
 	 * Writing on a stream
 	 * @param os the output stream for printing
 	 */
	void print(std::ostream & os) const;

	/**
 	 * Serialize the constraint in a Stream
 	 * @param o the output stream
 	 */
	bool serialize(std::ostream & os)
	{
		// TODO
		return false;
	};

	/**
 	 * Deserialize the constraint in a Stream
 	 * @param i the input stream
 	 */
	bool deserialize(std::istream & i)
	{
		// TODO
		return false;
	};

	/**
 	 * Compute the variable of the constraint in a set var
 	 * @param v the set of var where variables are put
 	 */
	void toVariables(VarImplSet & v);

	/**
 	 * indicates to the variable which SearchTree will be used
 	 * @param st the search space used for the computation
 	 */
	void initVariableImplementation(SearchTree & searchTree);

	/**
 	 * Returns the number of occurrences of v in *this
 	 * @param v the RealVarImplementation that we need the multiplicity
 	 * @return the multiplicity of v
 	 */
	int multiplicity(VariableImpl & v) const;


	/**
 	 * Give the type of the model
 	 * @return a string that contains the name of the type
 	 */
	virtual std::string type() const = 0;

	// ishii
	void reset()
	{
		m_vars.clear();
	}

protected:
	// @var the internal representation of the constraint
	ConstraintRep *m_rep;

	// @var Variables occurring in this constraint
	VarImplSet m_vars;
};


/**
 * @ingroup Constraint
 * @class ConstraintRelationRep
 * @brief Base class for evaluable constraint representation
 */
class ConstraintRelationRep
{
public:
	/**
 	 * Constructor
 	 */
	ConstraintRelationRep ()
	{
	}

	/**
 	 * Destructor
 	 */
	virtual
	~ConstraintRelationRep ()
	{
	}

	/// @name Satisfaction methods
	//@{
	/// Returns true if the constraint is violated by the current box
	bool isViolated() const
	{
		return !isPossiblySatisfied();
	}

	/// Returns true if violation cannot be proved
	virtual bool isPossiblySatisfied() const = 0;

	/// Returns true if the constraint is satisfied for all domain values
	virtual bool isCertainlySatisfied() const = 0;
	//@}
};

/**
 * @ingroup Constraint
 * @class ConstraintRelation
 * @brief Base class for constraints (container for variables)
 */
class ConstraintRelation
{
public:
	/**
 	 * Constructor
 	 */
	ConstraintRelation ()
	{
	}

	/**
 	 * Destructor
 	 */
	virtual
	~ConstraintRelation ()
	{
	}

	/// @name Satisfaction methods
	//@{
	/// Returns true if the constraint is violated by the current box
	bool isViolated() const
	{
		return !isPossiblySatisfied();
	}

	/// Returns true if violation cannot be proved
	virtual bool isPossiblySatisfied() const
	{
		return _rep->isPossiblySatisfied();
	}


	/// Returns true if the constraint is satisfied for all domain values
	virtual bool isCertainlySatisfied() const
	{
		return _rep->isCertainlySatisfied();
	}
	//@}

protected:
	// @var the computable test
	ConstraintRelationRep *_rep;
};

/**
 * @ingroup Constraint
 * @class SetOfConsraints
 * @brief Set of constraints
 *
 * Defined as std::set<Constraint*,ConstraintComparator>
 */
typedef std::set<Constraint *> SetConstraints;

/**
 * @ingroup Constraint
 * @class VectorOfConsraints
 * @brief Vector of constraints
 *
 * Defined as std::vector<Constraint*>
 */
typedef std::vector<Constraint *> VecConstraints;

END_NAMESPACE_ELISA

/** @relates elisa::Constraint
 * @brief Output of constraint on a stream
 */
inline std::ostream &
operator<<(std::ostream & os, const elisa::Constraint & c)
{
	c.print(os);
	return os;
}
#endif // ELISA_CONSTRAINT_H
